(declare-fun a (Int) Int)
(declare-fun b (Int) Int)
(declare-fun c (Int) Int)
(declare-fun d () Int)
(declare-fun h () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun i () Int)
(assert (let ((g d)(j h)(bb i)(bi d)(bj 0)(cm (b h))(dw h)(dz (c f))(eb (+ d i))(ec (+ d h))) (and (or (and (distinct dz bb e) (= bi bj) (= cm f i)) (= dw f)) (distinct d e) (distinct h e i) (< d 7) (< h 7) (< (c (ite (< eb 7) eb d)) (c (ite (< ec 7) ec d))))))
(check-sat)
